Search Results

Documents authored by Dowek, Gilles

Document
DOI: 10.4230/LIPIcs.FSCD.2022.21
Linear Lambda-Calculus is Linear

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.
Cite as

Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Linear Lambda-Calculus is Linear}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21},
  URN =		{urn:nbn:de:0030-drops-163024},
  doi =		{10.4230/LIPIcs.FSCD.2022.21},
  annote =	{Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.20
Some Axioms for Mathematics

Authors: Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.
Cite as

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois},
  title =	{{Some Axioms for Mathematics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20},
  URN =		{urn:nbn:de:0030-drops-142581},
  doi =		{10.4230/LIPIcs.FSCD.2021.20},
  annote =	{Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.14
Proof Normalisation in a Logic Identifying Isomorphic Propositions

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We define a fragment of propositional logic where isomorphic propositions, such as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Cite as

Alejandro Díaz-Caro and Gilles Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2019.14,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Proof Normalisation in a Logic Identifying Isomorphic Propositions}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.14},
  URN =		{urn:nbn:de:0030-drops-105210},
  doi =		{10.4230/LIPIcs.FSCD.2019.14},
  annote =	{Keywords: Simply typed lambda calculus, Isomorphisms, Logic, Cut-elimination, Proof-reduction}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.109
Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory

Authors: Gilles Dowek

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We define a notion of model for the lambda Pi-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the lambda Pi-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions.
Cite as

Gilles Dowek. Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 109:1-109:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dowek:LIPIcs.ICALP.2017.109,
  author =	{Dowek, Gilles},
  title =	{{Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{109:1--109:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.109},
  URN =		{urn:nbn:de:0030-drops-73919},
  doi =		{10.4230/LIPIcs.ICALP.2017.109},
  annote =	{Keywords: model, proof reduction, Simple type theory, Calculus of constructions}
}
Document
DOI: 10.4230/DagRep.6.10.75
Universality of Proofs (Dagstuhl Seminar 16421)

Authors: Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe

Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16421 "Universality of Proofs" which took place October 16-21, 2016. The seminar was motivated by the fact that it is nowadays difficult to exchange proofs from one proof assistant to another one. Thus a formal proof cannot be considered as a universal proof, reusable in different contexts. The seminar aims at providing a comprehensive overview of the existing techniques for interoperability and going further into the development of a common objective and framework for proof developments that support the communication, reuse and interoperability of proofs. The seminar included participants coming from different fields of computer science such as logic, proof engineering, program verification, formal mathematics. It included overview talks, technical talks and breakout sessions. This report collects the abstracts of talks and summarizes the outcomes of the breakout sessions.
Cite as

Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe. Universality of Proofs (Dagstuhl Seminar 16421). In Dagstuhl Reports, Volume 6, Issue 10, pp. 75-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{dowek_et_al:DagRep.6.10.75,
  author =	{Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian},
  title =	{{Universality of Proofs (Dagstuhl Seminar 16421)}},
  pages =	{75--98},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{10},
  editor =	{Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.10.75},
  URN =		{urn:nbn:de:0030-drops-69514},
  doi =		{10.4230/DagRep.6.10.75},
  annote =	{Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact